$\forall$${\it ds}$:(Id$\rightarrow$Type\{i\}), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type\{i\}), $A$, $B$:Type\{i\}. \\[0ex]component\{i:l\}(${\it ds}$; ${\it da}$; $A$; $B$) $\in$ Type\{i'\}